from cheqed.core import term, formula

class ExpansionError(Exception):
    pass

class SimplificationError(Exception):
    pass

class RequireError(Exception):
    pass

def require_class(obj, cls):
    if obj.operator != cls.operator:
        raise RequireError()
    
def expand_existential(form):
    require_class(form, formula.Existential)
    return formula.Negation(formula.Universal(form.args[0],
                                              formula.Negation(form.args[1])))
    
def simplify_existential(form):
    require_class(form, formula.Negation)
    require_class(form[0], formula.Universal)
    require_class(form[0][1], formula.Negation)

    return formula.Existential(form[0][0], form[0][1][0])    

def expand_conjunction(form):
    require_class(form, formula.Conjunction)
    return (formula.Negation(formula.Disjunction(
                formula.Negation(form.args[0]),
                formula.Negation(form.args[1]))))

def simplify_conjunction(form):
    require_class(form, formula.Negation)
    require_class(form[0], formula.Disjunction)
    require_class(form[0][0], formula.Negation)
    require_class(form[0][1], formula.Negation)

    return formula.Conjunction(form[0][0][0], form[0][1][0])

def expand_conditional(form):
    require_class(form, formula.Conditional)
    return formula.Disjunction(formula.Negation(form.args[0]), form.args[1])

def simplify_conditional(form):
    require_class(form, formula.Disjunction)
    require_class(form[0], formula.Negation)
    return formula.Conditional(form[0][0], form[1])

def expand_biconditional(form):
    require_class(form, formula.Biconditional)
    return (formula.Conjunction(
            formula.Conditional(form.args[0], form.args[1]),
            formula.Conditional(form.args[1], form.args[0])))

def simplify_biconditional(form):
    require_class(form, formula.Conjunction)
    require_class(form[0], formula.Conditional)
    require_class(form[1], formula.Conditional)
    if form[0][0] != form[1][1] \
       or form[0][1] != form[1][0]:
        raise ValueError()

    return formula.Biconditional(form[0][0], form[0][1])

def expand_separation(form):
    require_class(form, formula.Relation)
    if form.name != 'contains': raise RequireError()
    if len(form.args) != 2: raise RequireError()
    if form.args[1].__class__ != term.Separation: raise RequireError()

    sep = form.args[1]
    return (formula.Conjunction(
            formula.Relation('contains', form.args[0], sep.domain),
            sep.formula.substitute(form.args[0], sep.variable)))

def simplify_separation(form):
    raise RequireError('simplifying a separation statement is difficult.')

expansions = [
    expand_conjunction,
    expand_conditional,
    expand_biconditional,
    expand_existential,
    expand_separation,
    ]

conversions = [
    simplify_conjunction,
    simplify_conditional,
    simplify_biconditional,
    simplify_existential,
    simplify_separation,
    ]

def expand(form):
    for exp in expansions:
        try:
            return exp(form)
        except RequireError:
            pass

    raise ExpansionError('No expansion applies to formula "%s"' % str(form))

def simplify(form):
    for conv in conversions:
        try:
            return conv(form)
        except RequireError:
            pass

    raise SimplificationError('No simplification applies to formula "%s"'
                              % str(form))
